nLab Sierpinski space

Definition

In impredicative mathematics

Definition

The Sierpiński space $\Sigma$ is the topological space

1. whose underlying set has two elements, say $\{0,1\}$,

2. whose set of open subsets is $\left\{ \emptyset, \{1\}, \{0,1\} \right\}$.

(We could exchange “0” and “1” here, the result would of course be homeomorphic).

Equivalently we may think of the underlying set as the set of classical truth values $\{\bot, \top\}$, equipped with the specialization topology, in which $\{\bot\}$ is closed and $\{\top\}$ is an open but not conversely.

Remark

In constructive mathematics, it is important that $\{\top\}$ be open (and $\{\bot\}$ closed), rather than the other way around. Indeed, the general definition (since we can't assume that every element is either $\top$ or $\bot$) is that a subset $P$ of $\Sigma$ is open as long as it is upward closed: $p \Rightarrow q$ and $p \in P$ imply that $q \in P$. The ability to place a topology on $\Top(X,\Sigma)$ is fundamental to abstract Stone duality, a constructive approach to general topology.

In predicative constructive mathematics

Definition

The Sierpiński space $\Sigma$ is the initial $\sigma$-frame.

As a higher inductive type

In type theory, as a higher inductive type Sierpinski space $\Sigma$ is generated by the following constructors:

• A type $\Sigma$,
• A top term $1:\Sigma$
• A meet operation $(-)\wedge(-): \Sigma \times \Sigma \to \Sigma$
• A left unit identity for meet
  $$m_\lambda:\prod_{a:\Sigma} 1 \wedge a = a$$
• A right unit identity for meet
  $$m_\rho:\prod_{a:\Sigma} a \wedge 1 = a$$
• A associative identity for meet
  $$m_\alpha:\prod_{a:\Sigma} \prod_{b:\Sigma} \prod_{c:\Sigma} (a \wedge b) \wedge c = a \wedge (b \wedge c)$$
• A commutative identity for meet
  $$m_\kappa:\prod_{a:\Sigma} \prod_{b:\Sigma} a \wedge b = b \wedge a$$
• An idempotent identity for meet
  $$m_\iota:\prod_{a:\Sigma} a \wedge a = a$$
• A bottom term $0:\Sigma$
• A join operation $(-)\vee(-): \Sigma \times \Sigma \to \Sigma$
• A left unit identity for join
  $$j_\lambda:\prod_{a:\Sigma} 0 \vee a = a$$
• A right unit identity for join
  $$j_\rho:\prod_{a:\Sigma} a \vee 0 = a$$
• A associative identity for join
  $$j_\alpha:\prod_{a:\Sigma} \prod_{b:\Sigma} \prod_{c:\Sigma} (a \vee b) \vee c = a \vee (b \vee c)$$
• A commutative identity for join
  $$j_\kappa:\prod_{a:\Sigma} \prod_{b:\Sigma} a \vee b = b \vee a$$
• An idempotent identity for join
  $$j_\iota:\prod_{a:\Sigma} a \vee a = a$$
• A meet-join absorption identity
  $$m_j:\prod_{a:\Sigma} \prod_{b:\Sigma} a \wedge (a \vee b) = a$$
• A join-meet absorption identity
  $$j_m:\prod_{a:\Sigma} \prod_{b:\Sigma} a \vee (a \wedge b) = a$$
• A sequential join function:
  $$\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to \Sigma) \to \Sigma$$
• An ascending sequence condition:
  $$s: \prod_{n:\mathbb{N}} \prod_{s:\mathbb{N} \to \Sigma} s(n) \wedge \left(\Vee_{i:\mathbb{N}} s(i)\right) = s(n)$$
• A sequential least upper bound condition:
  $$l: \prod_{x:\Sigma} \prod_{s:\mathbb{N} \to \Sigma} \left(\prod_{n:\mathbb{N}} s(n) \wedge x = s(n)\right) \to \left(\left(\Vee_{n:\mathbb{N}} s(n)\right) \wedge x = \Vee_{n:\mathbb{N}} s(n)\right)$$
• A function
  $$\mathcal{t}:(\Sigma \times (\mathbb{N} \to \Sigma)) \to \mathbb{N} \to \Sigma$$
• A dependent function
  $$p:\prod_{x:\Sigma} \prod_{s:\mathbb{N} \to \Sigma} \mathcal{t}(x,s)(n) = x \wedge s(n)$$
• A sequentially distributive condition:
  $$d: \prod_{x:\Sigma} \prod_{s:\mathbb{N} \to \Sigma} x \wedge \left(\Vee_{n:\mathbb{N}} s(n)\right) = \Vee_{n:\mathbb{N}} \mathcal{t}(x,s)(n)$$
• A 0-truncator
  $$\tau_0: \prod_{a:\Sigma} \prod_{b:\Sigma} isProp(a=b)$$

As a higher inductive-inductive type

The Sierpinski space $\Sigma$ is inductively generated by

• a term $\bot:\Sigma$
• a binary operation $(-)\vee(-):\Sigma \times \Sigma \to \Sigma$
• a function $\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to \Sigma) \to \Sigma$
• a term $\top:\Sigma$
• a binary operation $(-)\wedge(-):\Sigma \times \Sigma \to \Sigma$

and the partial order type family $\leq$ is simultaneously inductively generated by

• a family of dependent terms

  $$a:\Sigma, b:\Sigma \vdash \pi(a,b):isProp(a \leq b)$$

  representing that each type $a \leq b$ is a proposition.

• a family of dependent terms

  $$a:\Sigma \vdash \rho(a):a \leq a$$

  representing the reflexive property of $\leq$.

• a family of dependent terms

  $$a:\Sigma, b:\Sigma, c:\Sigma \vdash \tau(a, b, c):(a \leq b) \times (b \leq c) \to (a \leq c)$$

  representing the transitive property of $\leq$.

• a family of dependent terms

  $$a:\Sigma, b:\Sigma \vdash \sigma(a, b):(a \leq b) \times (b \leq a) \to (a = b)$$

  representing the anti-symmetric property of $\leq$.

• a family of dependent terms

  $$a:\Sigma \vdash t(a):\bot \leq a$$

  representing that $\bot$ is initial in the poset.

• three families of dependent terms

  $$a:\Sigma, b:\Sigma \vdash i_a(a, b):a \leq a \vee b$$
  $$a:\Sigma, b:\Sigma \vdash i_b(a, b):b \leq a \vee b$$
  $$a:\Sigma, b:\Sigma, (-)\oplus(-):\Sigma \times \Sigma \to \Sigma, i_a(a, b):a \leq a \oplus b, i_b(a, b):b \leq a \oplus b \vdash i(a,b):(a \vee b) \leq (a \oplus b)$$

  representing that $\vee$ is a coproduct in the poset.

• two families of dependent terms

  $$n:\mathbb{N}, s:\mathbb{N} \to \Sigma \vdash i(n, s):s(n) \leq \Vee_{n:\mathbb{N}} s(n)$$
  $$x:\Sigma, s:\mathbb{N} \to \Sigma \vdash i(s, x):\prod_{n:\mathbb{N}}(s(n) \leq x) \to \left(\Vee_{n:\mathbb{N}} s(n) \leq x\right)$$

  representing that $\Vee$ is a denumerable/countable coproduct in the poset.

• a family of dependent terms

  $$a:\Sigma \vdash t(a):a \leq \top$$

  representing that $\top$ is terminal in the poset.

• three families of dependent terms

  $$a:\Sigma, b:\Sigma \vdash p_a(a, b):a \wedge b \leq a$$
  $$a:\Sigma, b:\Sigma \vdash p_b(a, b):a \wedge b \leq b$$
  $$a:\Sigma, b:\Sigma, (-)\otimes(-):\Sigma \times \Sigma \to \Sigma, p_a(a, b):a \leq a \otimes b, p_b(a, b):b \leq a \otimes b \vdash p(a,b):(a \otimes b) \leq (a \wedge b)$$

  representing that $\wedge$ is a product in the poset.

• a family of dependent terms

  $$x:\Sigma, s:\mathbb{N} \to \Sigma \vdash i(s, x):\left(\prod_{n:\mathbb{N}}(s(n) \leq x)\right) \to \left(\Vee_{n:\mathbb{N}} s(n) \leq x\right)$$

  representing the countably infinitary distributive property.

Properties

As a topological space

This Sierpinski space

• is a contractible space;

• is a locally contractible space;

• has a focal point;

• is a sober topological space (but not T1).

According properties are inherited by the Sierpinski topos and the Sierpinski (∞,1)-topos over $Sierp$.

As a classifer for open/closed subspaces

The Sierpinski space $S$ is a classifier for open subspaces of a topological space $X$ in that for any open subspace $A$ of $X$ there is a unique continuous function $\chi_A: X \to S$ such that $A = \chi_A^{-1}(\top)$.

Dually, it classifies closed subsets in that any closed subspace $A$ is $\chi_A^{-1}(\bot)$. Note that the closed subsets and open subsets of $X$ are related by a bijection through complementation; one gets a topology on the set of either by identifying the set with $\Top(X,\Sigma)$ for a suitable function space topology. (This part does not work as well in constructive mathematics.)

Related concepts

• empty space, point space

• Cantor space

• Sierpinski topos, Sierpinski (∞,1)-topos

• Stone duality

• separation axioms in terms of lifting properties

• In synthetic topology, an analogue of the Sierpinski space is called a dominance.

• $\sigma$-frame

References

• Wikipedia, Sierpinski space

• Paul Taylor, Foundations for computable topology – 7 The Sierpinski space (html)

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

• Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (abs:1610.09254)

• Martin Escardó, Cory Knapp, Partial Elements and Recursion via Dominances in Univalent Type Theory (pdf)

• Andrej Bauer, Davorin Lešnik, Metric spaces in synthetic topology (pdf)